basic
BiLinear(T;pl;tm)
== a, x, y:T.
== (a tm (x pl y)) = ((a tm x) pl (a tm y)) & ((x pl y) tm a) = ((x tm a) pl (y tm a)) 

latex

---

clarification:

basic
BiLinear(T;pl;tm)
== a:T.
== x:T, y:T.
== (a tm (x pl y)) = ((a tm x) pl (a tm y))  T & ((x pl y) tm a) = ((x tm a) pl (y tm a))  T 

latex

Up	gen algebra 1
Wellformedness Lemmas	bilinear wf
Definitions	x:A. B(x), P & Q, x f y